$\forall$$T$:Type, $P$:($T$$\rightarrow$prop\{i:l\}), $L_{1}$,$L_{2}$:($T$ List).
\\[0ex]l\_all(append($L_{1}$; $L_{2}$); $T$; $x$.$P$($x$)) $\Leftarrow\!\Rightarrow$ (l\_all($L_{1}$; $T$; $x$.$P$($x$)) $\wedge$ l\_all($L_{2}$; $T$; $x$.$P$($x$)))